|
Automated proof checking is the process of using software for checking proofs for correctness. It is one of the most developed fields in automated reasoning. Automated proof checking differs from automated theorem proving in that automated proof checking simply mechanically checks the formal workings of an existing proof, instead of trying to develop new proofs or theorems itself. Because of this, the task of automated proof verification is much simpler than that of automated theorem proving, allowing automated proof checking software to be much simpler than automated theorem proving software. Because of this small size, some automated proof checking systems can have less than a thousand lines of core code, and are thus themselves amenable to both hand-checking and automated software verification. The Mizar system, HOL Light, and Metamath are examples of automated proof checking systems. Automated proof checking can be done either as a batch operation, or interactively, as part of an interactive theorem proving system. ==Field journals and conferences== * ''Intelligent Computer Mathematics'' * ''Journal of Formalized Reasoning'' * ''Interactive Theorem Proving'' * ''Formalized Mathematics'' * ''Studies in Logic, Grammar and Rhetoric'' 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Automated proof checking」の詳細全文を読む スポンサード リンク
|